COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	%test of maxtex
C00004 ENDMK
C⊗;
%test of maxtex
\input kermac
\magnify{1500}

\ctrline{Denigrating modal (especially temporal) logic}

\yskip
Manna and Pnueli {\it ``The Modal Logic of Programs''} AIM-330, CS-751, say:

\yskip
\noindent p. 3

\displaypar{\hangindent 20pt \it ``In spite of these
 qualifications there are some obvious advantages in
the introduction and use of modal formalisms.  It allows an explicit
discrimination of one para\-meter as being appreciably more significant than
all the others, and makes the dependence on that para\-meter implicit.''}

\yskip
Indeed one parameter (time in the case they discuss) is more important
than the others.  Unfortunately for modal logic, treating it by modal
operators discriminates against it rather than in its favor.

\yyskip
\noindent p. 11

	{\it ``With these conventions we will proceed to express meaningful
prop\-erties of programs and their executions.  Remember that under our
rules of the game we are never to mention  R  explicitly.''}

\yskip
Thus Manna and Pnueli can prove properties of programs with one hand tied behind
each of their backs.

\par\vfill\end